…gaps

vcl-ut has FIVE cargo workspace roots. CI covered three of them, and the
two it missed had stopped compiling without anyone noticing.

WHAT ROTTED

`ast::Statement` gained the S1 consonance field `verb` (Select / Inspect /
Verify / Assert / Declare / Retract / Merge / Split / Normalise) — the
consonance turn itself. Two downstream crates were never updated:

  src/interface/attest          E0063: missing field `verb`
  src/interface/recompute-wasm  E0063: missing field `verb`

In both cases only the in-file `#[cfg(test)]` module was stale; the
libraries still built. That is why nothing downstream complained — 12
tests had simply stopped running, in the crates carrying the attestation
and recompute boundaries.

Fixed by supplying `verb: Verb::Select` at both sites. Both constructions
are the bare `SELECT * FROM STORE "s"` case and both already used the full
eight-modality `OctadSchema`, so the octad was already correct there; only
the verb was missing.

  attest          9 tests, now green
  recompute-wasm  3 tests, now green

Their Cargo.lock files had also drifted (recompute-wasm's recorded only the
two in-repo path crates and no external deps at all — it had not been
resolved since its manifest grew dependencies). Regenerated and committed.

WHY IT ROTTED — coverage map, measured 2026-07-21

  /                              e2e.yml             PARTIAL (see below)
  /src/interface/parse           parse-gate.yml      full
  /src/interface/echidna-client  backend-matrix.yml  needs echidna sibling
  /src/interface/attest          NOTHING
  /src/interface/recompute-wasm  NOTHING

New satellite-crates-gate.yml gates the last two: clippy `-D warnings`
plus tests, over a matrix. Both were verified to pass `-D warnings` cleanly
before the gate was added, so this is a real gate that is green, not an
aspirational one. It mirrors parse-gate.yml's deliberate use of preinstalled
rustup over a third-party toolchain action.

`--locked` is deliberately omitted there for now, and the reason is recorded
in the workflow: the lockfiles are freshly regenerated after a long ungated
drift. It should be restored once a Dependabot cycle has run against them.

ALSO FIXED IN e2e.yml

1. The root job ran `--test property_test` + `--test integration_test` only:
   69 of the root workspace's 102 tests. Every test in tests/e2e_test.rs (20)
   and tests/fuzz_test.rs (13) was skipped. Now `cargo test --workspace
   --all-targets --locked`, verified locally at 102 passed / 0 failed.

2. Removed both "Provide echidna sibling" steps, which cloned a whole
   repository on every run for nothing. `src/interface` — the member that
   carries the external `echidna-core` path-dep — is deliberately not a root
   workspace member, so neither the root tests nor tests/e2e.sh ever resolve
   it. Verified with no sibling present: 102 tests pass, e2e.sh reports 19/19.
   echidna-client remains gated by backend-matrix.yml, which does need it.

CORRECTION TO AN EARLIER FINDING

An earlier read of this repository recorded "0 unit tests; root cargo test is
a fake gate". That was wrong, and was an artefact of truncating the log to its
last lines. The root crate is a re-export facade over fmt + lint, so per-crate
UNIT counts are legitimately zero and the entire surface lives in tests/.
The README's `tests-102 pass` badge is exact. Recorded in the e2e.yml header
so the same misreading is not repeated.

Verification:
  reuse lint                          -> compliant, 459/459
  23 workflows                        -> 0 malformed
  cargo test --workspace --locked     -> 102 passed
  cargo test (parse)                  -> 36 passed
  cargo test (attest)                 -> 9 passed
  cargo test (recompute-wasm)         -> 3 passed
  bash tests/e2e.sh                   -> 19/19, no echidna sibling
                                         150 tests total

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

The flagship explanatory document disagreed with the implementation on the
numbering, the vocabulary and the number of levels. All three are corrected
against `src/interface/parse/src/ast.rs` and `src/core/Levels.idr`, which are
canonical because the numbers are wire tags, not prose.

1. NUMBERING WAS OFF BY ONE

   Doc: Level 1 Parse ... Level 10 Linearity.
   Code: ParseSafe = 0 ... LinearSafe = 9, EpistemicSafe = 10.

   A reader who requested level 7 expecting Cardinality Safety would have got
   Effect-Tracking. Every heading, table and diagram shifted down by one; a
   mapping note added so old citations can be translated.

2. THE DOCUMENTED VOCABULARY DOES NOT PARSE

   The document taught `FETCH` and `REMOVE`. Neither appears anywhere in the
   parser. Measured against the real parser:

     FETCH users.name EFFECTS { Read }   -> REJECTED "expected keyword SELECT"
     REMOVE users WHERE ...              -> REJECTED "expected keyword SELECT"
     SELECT * FROM STORE main            -> parses, verb=Select
     ASSERT * FROM STORE main            -> parses, verb=Assert
     DECLARE * FROM STORE main           -> parses, verb=Declare

   The real keyword surface is SELECT / INSPECT / VERIFY / ASSERT / DECLARE /
   RETRACT / MERGE / SPLIT / NORMALISE. Replaced 19 FETCH and 3 REMOVE.

   The implementation is well AHEAD of the prose here: the consonance verbs
   are fully parseable and carry the right verb tag. Only the documentation
   was still speaking the pre-consonance language.

3. THERE ARE ELEVEN LEVELS, NOT TEN — AND THE ELEVENTH WAS UNDOCUMENTED

   L10 `EpistemicSafe` appeared in no document anywhere in the repository. It
   now has a full section, written from `Levels.idr` and `Decide` rather than
   invented: the four `EpistemicRequirement` forms, and the four conditions
   `epistemicConsistentStmt` actually decides (clause present; >=1 agent; every
   referenced agent declared; no direct ENTAILS cycle).

   Its two owed obligations are stated plainly rather than glossed —
   transitive ENTAILS-cycle detection and proposition well-typedness are
   disclosed residuals in VERIFICATION-STANCE.adoc. A safety level that
   overstates itself is worse than no level at all.

   L10 is also flagged as different in KIND. L0-L9 are safety properties: they
   rule out executions that go wrong. L10 is a warrant property: it rules out
   answers the engine is not entitled to give, though every step was
   well-typed. A passive store cannot need it — one witness cannot disagree
   with itself. A consonance engine over eight modal witnesses can.

   Correspondingly, the TypeLL inheritance diagram is corrected: L10 is NOT
   inherited from TypeLL. A UI panel has no federation and no warrant
   question. L10 originates in VCL-UT — the first level this domain
   contributed back to the theory rather than received from it.

4. NEW: THE UPPER LADDER HAS NO SURFACE SYNTAX (measured)

   `parse_statement` hardcodes proof_clause, effect_decl, version_const,
   linear_annot and epistemic_clause to None, while `infer_requested_level`
   awards L7-L10 on exactly those fields. So no parsed statement can reach
   them. Measured ceiling:

     L1  SELECT * FROM STORE a
     L4  SELECT * FROM STORE a WHERE GRAPH.x > 1
     L6  SELECT * FROM STORE a LIMIT 10
     --  EFFECTS / AS OF / USE ONCE / AGENTS  -> all rejected

   Highest level reachable from VCL source: L6. Ladder defines: L10.

   This is a DISCLOSED, fail-closed gap, not silent rot — the parser rejects
   EFFECTS with a message naming the P5a slice and issue #25 rather than
   accepting and ignoring it. Fail-closed is correct. But the honest claim is
   now recorded in the document: eleven levels are specified and proved; six
   are expressible.

Title changed from "The 10 Levels of Type Safety" to "The Levels of Type
Safety" — the count was the false part. The filename is left alone so no
existing link breaks; whether to rebrand around eleven levels is a naming
decision for the owner, not something to settle in a doc fix.

Verification:
  reuse lint -> compliant, 459/459
  all level headings cross-checked one-by-one against ast.rs SafetyLevel
  no residual "10 levels" / "levels 1-N" claims remain

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Naming, counts and status claims brought into line with what is measurably
true, following the owner's decision that VCL-UT = *Usage-Tracked* is canon
and that this repository is the source of truth for the level ladder.

README.adoc
  - Title and 18 body occurrences: VCL-total -> VCL-UT.
  - The "Ubiquitous Type-safe" gloss is removed and explicitly retired. Both
    superseded expansions ("Ubiquitous Type-safe", "-total") are named so they
    stop recirculating. Usage-Tracked is also the accurate one: what
    distinguishes this tier is that resource usage is tracked in the type
    system, L9 LinearSafe via QTT.
  - "-total" is noted as surviving in the crate name `vcl-total` and the Idris
    namespace `VclTotal`; renaming those is invasive and deliberately not
    bundled here.
  - Tests badge 102 -> 150. 102 was correct for the root workspace but counted
    only one of the five workspace roots. Measured: 102 root + 36 parse
    + 9 attest + 3 recompute-wasm.
  - "all 10 levels of type safety" -> eleven, L0-L10, with L10 EpistemicSafe
    identified as a warrant property rather than a safety property.
  - Added the honest qualification up front: eleven levels are specified and
    proved, six are expressible (surface-syntax ceiling is L6).
  - Pipeline diagram: "(10 progressive levels)" -> "(11 levels, L0-L10)".

  Left deliberately unchanged: the four "10 levels" references that describe
  TypeLL. Under the corrected framing those are correct — TypeLL defines
  L0-L9, exactly ten, and VCL-UT contributes the eleventh.

ROADMAP.adoc — rewritten, because nearly every claim was false
  - "Parser work not yet started" was false: a Rust parser exists with 36
    green tests, gated by parse-gate.yml under a SPARK-grade clippy set.
  - "Idris2 parser with totality proof" was never what shipped. The Idris
    corpus proves; the Rust port re-establishes independently.
  - Every milestone box was unchecked despite most of v0.1-v0.3 being done.
    Boxes now reflect measured state.
  - Level numbering corrected 1-10 -> L0-L10 throughout.
  - "VeriSimDB 6-modal query planner" -> octad transition planner.
  - Added a measured status table and a "Nearest Work" section ordered by
    value: surface syntax for L7-L10; wiring vclt-gate into VeriSimDB;
    discharging the two disclosed L10 residuals; retiring the HEXAD keyword.
  - New v0.4.0 milestone for the consonance level, which the old roadmap had
    no place for at all.

Cargo manifests (8 files)
  - repository = ".../vql-ut" -> ".../vcl-ut".

  Correction to an earlier note: that URL does not 404. GitHub still redirects
  vql-ut -> vcl-ut after the rename. It is stale rather than broken, and the
  reason to fix it is that the redirect stops working if the old name is ever
  reused. Measured with `gh api repos/hyperpolymath/vql-ut`, which returns
  full_name "hyperpolymath/vcl-ut".

  CHANGELOG.md's "still hyperpolymath/vql-ut" line is left alone: it is a
  dated historical entry, not a live claim.

Verification:
  reuse lint                       -> compliant, 459/459
  cargo test --workspace --locked  -> 102 passed

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

…lication

The strategic deliverable. Two strands kept deliberately separate because they
have different success conditions: Strand A succeeds if the theoretical claim
is novel and defensible; Strand B succeeds if VeriSimDB is measurably safer.
Neither implies the other.

STRAND A — the theoretical claim

Argues that consonance languages are a distinct class, not query languages
with extra types, on three grounds: statements are propositions and epistemic
requests rather than read requests; retraction is not deletion and drift is a
typed condition rather than an error; and well-typedness stops being
sufficient once several modal witnesses can disagree.

The gap in the world is stated honestly. Type-safe query languages are a
crowded, mature field — LINQ, Quill, Diesel, jOOQ, TypeQL, EdgeQL for L0-L5,
and substantial literature for effects, temporal, linear and cardinality. A
"ten levels of query safety" paper enters that field as a thorough synthesis
and will be read as one. What none of them do is type WARRANT: every one
assumes a single source of truth that cannot disagree with itself. Epistemic
logic, provenance and truth-maintenance all exist, but beside the query path —
never as a type that can refuse a statement.

The decisive evidence came from the code rather than from taste. The ladder
has eleven levels; the eleventh is not a query-safety property; and it is the
one level NOT inherited from TypeLL, because a UI panel has no federation and
so no warrant question. A framework whose eleventh member does not fit its own
name is telling you the name is wrong.

WHITEPAPER REFRAME IS A PROPOSAL, NOT AN EXECUTED REWRITE

Deliberate. The direction is settled, but how a paper argues its claim is the
author's call and is the least testable, highest-blast-radius change available
here. The 1,909-line .tex is untouched. What is offered is a section-by-section
structure and a complete draft abstract, for approval first.

STRAND B — the VeriSimDB application

Opens with the uncomfortable fact: VCL-UT delivers nothing to VeriSimDB at
runtime today. The proof corpus is real, the parser is real and gated, the
gate binary exists and Contract v1 is frozen — but the seam is built on one
side only. The producer is finished and the consumer was never written.

Defends the subprocess/JSON-line seam against the obvious objection that it
looks unfashionable, using evidence from this repository: src/interface's
external path-dep on an echidna sibling is exactly the build coupling the
CLI seam avoids, and it is why echidna-client cannot even be covered by
Dependabot.

Sets out what VeriSimDB actually gets — a fail-closed admissibility check
before statements touch consonance state; one level ladder instead of two
divergent ones; independently-verifiable attestation; and vocabulary
discipline — and gives a migration path that keeps VeriSimDB's genuinely good
ReScript surface parser and diagnostics while replacing only the verdict.

Two concrete defects, both located precisely:
  - VCLTypeChecker.res:60 builds the default context with six modalities
    though the type admits eight. Provenance and Spatial are silently absent
    from every default type-check. The hexad-to-octad migration reached the
    variants and stopped before the defaults and the names — HexadType is
    still the type name in four places.
  - The seam is unwired (zero vclt-gate references in verisim-api/src/vcl.rs).

Sequenced plan, ordered by value per unit of risk, with the repository each
item belongs to marked — items 3-5 are VeriSimDB changes and cannot be
committed from this repository.

Closes with a falsification section, so the plan can be argued with rather
than assumed: if VeriSimDB's ReScript checker is materially more capable than
the corpus, "vcl-ut is source of truth" costs capability; if subprocess
latency is material on the hot path, the CLI seam is wrong and should be
measured BEFORE the wiring work rather than after; and if the consonance claim
has prior art under another name, Strand A weakens to a synthesis claim. The
prior-art search behind the gap argument was not exhaustive and says so.

Verification:
  reuse lint -> compliant, 460/460
  every factual claim in the Ground Truth table measured against the working
  tree on 2026-07-21, including the two VeriSimDB defects

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>